Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

RFC: Global Conditions #2516

Merged
merged 9 commits into from
Jun 27, 2023
Merged

Conversation

adpaco-aws
Copy link
Contributor

@adpaco-aws adpaco-aws commented Jun 12, 2023

Description of changes:

This RFC proposes a new section in Kani's output to summarize the status of properties that depend on other properties, referred to as "Global Conditions". Originally, I wanted this change to be part of #2299, but then I realized a small RFC might be appropriate.

Resolved issues:

N/A

Testing:

  • How is this change tested? N/A

  • Is this a refactor change? N/A

Checklist

  • Each commit message has a non-empty body, explaining why the change was made
  • Methods or procedures are documented
  • Regression or unit tests are included, or existing tests cover the modified code
  • My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@adpaco-aws adpaco-aws added the T-RFC Label RFC PRs and Issues label Jun 12, 2023
@adpaco-aws adpaco-aws requested a review from a team as a code owner June 12, 2023 22:20
Copy link
Contributor

@celinval celinval left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It makes sense.

rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0007-global-conditions.md Show resolved Hide resolved
rfc/src/rfcs/0007-global-conditions.md Show resolved Hide resolved
@zhassan-aws
Copy link
Contributor

Copy link
Contributor

@zhassan-aws zhassan-aws left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I cannot think of other "Global Conditions" that may be introduced in the future. Do you have any in mind? If not, I think for the case of fail_uncoverable, it would be obvious why verification fails when the unsatisfiable cover properties are included in the "Failed Checks" section. In which case, a new section may not be needed.

rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
@adpaco-aws adpaco-aws self-assigned this Jun 13, 2023
Copy link
Contributor

@karkhaz karkhaz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems to me that there are two commonalities in @adpaco-aws's examples of should_panic and fail_uncoverable:

  • Their statuses are derived entirely from the status of other properties, and not directly a result from the SAT solver
  • They are of the form "{panic,coverage} did not happen along any path" rather than "{overflow} happened along some path".

Would you expect these to be true for other global conditions that might be added in the future? I think the first bullet point is how you're defining hyperproperty/global condition, but I think the second bullet point is more relevant to users and might be a good reason to separate hyperproperties out from regular ones.

rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
rfc/src/rfcs/0007-global-conditions.md Outdated Show resolved Hide resolved
@adpaco-aws
Copy link
Contributor Author

I cannot think of other "Global Conditions" that may be introduced in the future. Do you have any in mind?

Yes, the check for expectations on individual properties mentioned here could be implemented as a global condition. Another global condition that I think could be interesting for users would check that specific properties (e.g., user-defined assertions) are not unreachable. This can already be manually done by adding cover statements, but that isn't always an option (because the user may not want to add them) and users may not realize they are unreachable if they appear in deep places in the call graph.

But one of the cool things about global conditions is that we could also define them for existing properties. For example, we could have a memory safety condition that summarizes the status memory-safety checks (and hide them from RESULTS if all went well). Or do the same for unwinding assertions, as @celinval mentioned. If we did that, this section could become the main component of Kani's output.

@celinval
Copy link
Contributor

I cannot think of other "Global Conditions" that may be introduced in the future. Do you have any in mind?

Yes, the check for expectations on individual properties mentioned here could be implemented as a global condition. Another global condition that I think could be interesting for users would check that specific properties (e.g., user-defined assertions) are not unreachable. This can already be manually done by adding cover statements, but that isn't always an option (because the user may not want to add them) and users may not realize they are unreachable if they appear in deep places in the call graph.

But one of the cool things about global conditions is that we could also define them for existing properties. For example, we could have a memory safety condition that summarizes the status memory-safety checks (and hide them from RESULTS if all went well). Or do the same for unwinding assertions, as @celinval mentioned. If we did that, this section could become the main component of Kani's output.

Please do replace the memory safety and arithmetic checks by global conditions! :) It would result in a much cleaner output.

One thing I'm missing in this RFC is an explanation on how the user could easily find the root cause of the failing global condition. For example, for the fail_uncovered, do we expect users to go inspect all the covers or can we print the uncovered ones the same way we print failed checks at the end?

@adpaco-aws
Copy link
Contributor Author

They are of the form "{panic,coverage} did not happen along any path" rather than "{overflow} happened along some path".

Actually, the should_panic condition expresses "there exists at least one path with an assertion-related failure". I'm defining global conditions as in the first item because that's what I'm trying to generalize here, and I'd expect new ones to follow this rule but I can't guarantee it. But that's OK, we can always go back to this RFC and update it 😄

@adpaco-aws
Copy link
Contributor Author

One thing I'm missing in this RFC is an explanation on how the user could easily find the root cause of the failing global condition. For example, for the fail_uncovered, do we expect users to go inspect all the covers or can we print the uncovered ones the same way we print failed checks at the end?

That's a great point, but I'm concerned about the output getting longer and less comprehensible if we include that change in this RFC. My preference here would be to keep it simple for now, but I'm happy to talk about it.

@celinval
Copy link
Contributor

One thing I'm missing in this RFC is an explanation on how the user could easily find the root cause of the failing global condition. For example, for the fail_uncovered, do we expect users to go inspect all the covers or can we print the uncovered ones the same way we print failed checks at the end?

That's a great point, but I'm concerned about the output getting longer and less comprehensible if we include that change in this RFC. My preference here would be to keep it simple for now, but I'm happy to talk about it.

I agree that our output is pretty long and it needs refactoring ASAP.

However, I think that printing the uncovered statements at the end will alleviate the problem of our super verbose output. At least the information that the user really needs is readily available at the end of the report, just like failed properties.

@adpaco-aws
Copy link
Contributor Author

However, I think that printing the uncovered statements at the end will alleviate the problem of our super verbose output. At least the information that the user really needs is readily available at the end of the report, just like failed properties.

Makes sense. I've been extending the current implementation (in #2532) to use the function that reports failed checks for standard verification jobs, but it needs improvements. For example, for a simple harness which contains an unreachable cover statement we get this information:

RESULTS:
Check 1: harness_uncoverable.cover.1
         - Status: UNREACHABLE
         - Description: "cover location"
         - Location: tests/ui/fail-uncoverable/uncoverable/test.rs:13:9 in function harness_uncoverable

GLOBAL CONDITIONS:
 - fail_uncoverable: FAILURE (encountered one or more cover statements which were not satisfied)
Failed Checks: cover location

SUMMARY:
 ** 0 of 0 failed

 ** 0 of 1 cover properties satisfied (1 unreachable)


VERIFICATION:- FAILED (one or more global conditions failed)
Verification Time: 0.02321334s

Note that it only says "Failed Checks: cover location", but it doesn't attach a location despite showing it for the property because the trace doesn't refer to this location, causing us to return earlier. We should make some changes here, also because the "Failed Checks: " gets printed for each item (the results below are for tests/ui/should-panic-attribute/unexpected-failures/test.rs) which is causing the output to be cluttered and a little confusing:

SUMMARY:
 ** 3 of 18 failed
Failed Checks: panicked on the `1` arm!
 File: "/home/ubuntu/kani/tests/ui/should-panic-attribute/unexpected-failures/test.rs", line 18, in check
Failed Checks: panicked on the `0` arm!
 File: "/home/ubuntu/kani/tests/ui/should-panic-attribute/unexpected-failures/test.rs", line 17, in check
Failed Checks: shift distance too large

In any case, I agree with your point - I'll change the RFC with a new proposal to report these failed checks.

@celinval
Copy link
Contributor

Since this is an RFC, please wait for a second approval before merging.

Copy link
Contributor

@karkhaz karkhaz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Awesome. Thanks for working on this!!

Copy link
Contributor

@jaisnan jaisnan left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks :) !


## Summary

A new section in Kani's output to summarize the status of properties that depend on other properties. We use the term *global conditions* to refer to such properties.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

would "dependent conditions" be a better name than "global conditions" ?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So are global conditions solely defined as conjunctions of assert/cover statement or are there other ways of defining them ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure about the name.

Global conditions do not need to depend on assert/cover statements, and there should be other ways to define them. For example, one possibility we've discussed in the past is to have a memory-safety condition based on the result of all memory safety checks we currently produce.

## User Impact

The addition of new options that affect the overall verification result depending on certain property attributes demands some consideration.
In particular, the addition of a new option to fail verification if there are uncoverable (i.e., unsatisfiable or unreachable) `cover` properties (requested in [#2299](https://github.com/model-checking/kani/issues/2299)) is posing new challenges to our current architecture and UI.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What are the problems being addressed ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if you're asking about the problems being addressed in Kani (to enable global conditions) or the problems being addressed with the feature requested in #2299 .

If it's the former, then the problem is that Kani isn't flexible enough. Until the #[kani::should_panic] attribute was introduced, there was only one way to get a successful verification: making all checks pass (i.e., getting a SUCCESS status in each of the individual checks/properties). But users may want to verify other things, or define additional conditions for verification like we're doing here.

If it's the latter, then the problem is vacuity. We check the status for cover properties, but their status doesn't impact verification in any way. Some users want to additionally ensure that the predicates in cover are always satisfied - the option requested in #2299 is for them.

A `FAILED` status in any enabled global condition will cause verification to fail.
In that case, the overall verification result will point out that one or more global conditions failed, as in:

```
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it possible to list the basic conditions that failed to explain why a global condition failed ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it should be possible.

The request in [#2299](https://github.com/model-checking/kani/issues/2299) is essentially another global conditions, and we may expect more to be requested in the future.

In this RFC, we propose a new section in Kani's output focused on reporting global conditions.
The goal is for users to receive useful information about hyperproperties without it becoming overwhelming.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is "hyperproperties" meant as in "a property that relates two or more executions of the same program?"

- `fail_uncoverable`: SUCCESS (all cover statements were satisfied as expected)
```

A `FAILED` status in any enabled global condition will cause verification to fail.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are global conditions only enabled using special flags or can the user also define his own groups of dependent conditions ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please note that those are two separate questions:

  1. Are global conditions only enabled using special flags?: No. Some may be enabled using special flags. Others may be enabled using attributes. Others may use a combination. We don't put constrains on this at the moment.
  2. Can the user also define his own groups of dependent conditions?: No, the RFC doesn't contemplate this option at the moment. That would require a language to define conditions.


As mentioned earlier, we're proposing this change to help users understand global conditions and how they're determined.
In many cases, global conditions empower users to write harnesses which weren't possible to write before.
As an example, the `#[kani::should_panic]` attribute allowed users to write harnesses expecting panic-related failures.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

the documentation of should_panic does not really give a precise meaning to the check, i.e. it does not say if at least one execution must trigger a panic or if all executions must trigger a panic. How can it be modelled in terms of dependent conditions and statuses ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think we do that for any of the checks we currently produce. Regardless, I think it's well defined in here, and if you think otherwise I'm happy to do any editions you consider appropriate.


### Alternative: Global conditions as regular checks

One option we've considered in the past is to enable global conditions as a regular checks.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is a regular check ? kani::assert ? kani::cover ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Check is the simpler term we use to refer to properties. Running Kani on any will output something like this:

RESULTS:
Check 1: example.assertion.1
         - Status: <status>
         - Description: <description>
         - Location: <location>
[...]

So this refers to those checks/properties.


## Open questions

No open questions.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is it possible to give a more explicit and rigorous definition of global conditions ?

e.g. "a global condition is specified by a set of assert or cover statements and an aggregation function that computes a status for the global conditions from the statuses of the basic conditions."

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe? But it's definitely not that.

I'm actually thinking about growing the scope of global conditions to consider things other than other properties. For example, a timeout feature could be implemented a global condition. However, the current definition of global condition does not consider resources like memory or time, only verification properties.


A redesign of Kani's output is likely to change the style/architecture to report global conditions.

[^status-computation]: The results for global conditions would be computed during postprocessing based on the results of other checks.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

so the status of a global condition could differ when the switch --fail-uncoverable is activated vs not activated ?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No. The status computed for the condition itself won't differ. But activating the switch will simply cause the status of the global condition to affect the overall verification result.

adpaco-aws added a commit that referenced this pull request Jan 12, 2024
…tions (#2967)

This PR is the next step to rework/introduce the
`should_panic`/`fail_uncoverable` options as global conditions.

Until now, we haven't had a concrete proposal to do so other than the
implementation in #2532. This PR presents one for each option in their
respective RFCs. I'd like to agree on this design before starting the
code review for #2532.

Related to #1905 #2272 #2299 #2516
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
T-RFC Label RFC PRs and Issues
Projects
No open projects
Status: In Progress
Status: Done
Development

Successfully merging this pull request may close these issues.

7 participants